\begin{tabbing}
$\forall$\=$A_{1}$, $A_{2}$:Type, $l_{1}$, $l_{2}$:IdLnk, ${\it tg}_{1}$, ${\it tg}_{2}$:Id, ${\it ds}_{1}$, ${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]${\it conds}_{1}$:$k$:Knd fp$\rightarrow$ $V$:Type $\times$ (State(${\it ds}_{1}$)$\rightarrow$$V$$\rightarrow$($A_{1}$ + Top)),
\\[0ex]${\it conds}_{2}$:$k$:Knd fp$\rightarrow$ $V$:Type $\times$ (State(${\it ds}_{2}$)$\rightarrow$$V$$\rightarrow$($A_{2}$ + Top)).
\-\\[0ex]($\forall$$k$:Knd. ($\uparrow$$k$ $\in$ dom(${\it conds}_{1}$)) $\Rightarrow$ ($\uparrow$hasloc($k$;source($l_{1}$))))
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd. ($\uparrow$$k$ $\in$ dom(${\it conds}_{2}$)) $\Rightarrow$ ($\uparrow$hasloc($k$;source($l_{2}$))))
\\[0ex]$\Rightarrow$ ($\neg$(source($l_{1}$) = source($l_{2}$) $\in$ Id))
\\[0ex]$\Rightarrow$ ((rcv($l_{2}$,${\it tg}_{2}$) $\in$ fpf{-}domain(${\it conds}_{1}$)) $\Rightarrow$ ($A_{2}$ $\subseteq$r (${\it conds}_{1}$(rcv($l_{2}$,${\it tg}_{2}$)).1)))
\\[0ex]$\Rightarrow$ ((rcv($l_{1}$,${\it tg}_{1}$) $\in$ fpf{-}domain(${\it conds}_{2}$)) $\Rightarrow$ ($A_{1}$ $\subseteq$r (${\it conds}_{2}$(rcv($l_{1}$,${\it tg}_{1}$)).1)))
\\[0ex]$\Rightarrow$ triggersGlue($A_{1}$; $l_{1}$; ${\it tg}_{1}$; ${\it ds}_{1}$; ${\it conds}_{1}$) $\parallel$ triggersGlue($A_{2}$; $l_{2}$; ${\it tg}_{2}$; ${\it ds}_{2}$; ${\it conds}_{2}$)
\end{tabbing}